| Definitions | s = t, x:A  B(x),  x:A. B(x), E, {x:A| B(x)} , a:A fp B(a),  b, left + right, P  Q, f(a), strong-subtype(A;B), P   Q, ||as||, ccsucc-num(x), ES, Type, X  Y = 0, prior(X), a < b, loc(e), X(e), ccsucc-id(x), Id, cmd-history(e), nth_tl(n;as), csupdate-cmds(x), type List, x:A  B(x), P & Q, let x = a in b(x), A c B, update-antecedent{i:l}(es;Cmd;Sys;Config;u), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , chain_sys(Cmd), chain_config(),  , csupdate?(x), e   X, Unit, tt, inr x , "$token", ff, inl x , Atom, True, False,  ,  x:A. B(x), (e < e'), <a, b>, chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds)), e < e', (e <loc e'), valid-sys(es;Config;Sys;e),  A, ccsucc?(x), (x l), x dom(f), Void, x:A.B(x), P  Q, P Q, f  g, f(x)?z, vartype(i;x), state@i, State(ds), State(ds), {T}, EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd,   x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M),  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, constant_function(f;A;B), let x,y = A in B(x;y),  T,  , Sys(valid), Top, AbsInterface(A), t T, E(X), x.A(x), sys-cmds(x), t.1, i  j ,  , Outcome, A B, #$n, e(e1,e2].P(e), @e(x v), (last change to x before e), pred(e), e loc e' |
u:({e:E(Sys)|